(set-logic BV)
(synth-fun f ( (x (BitVec 64)) ) (BitVec 64)
((Start (BitVec 64)
((bvnot Start)
(bvxor Start Start)
(bvand Start Start)
(bvor Start Start)
(bvneg Start)
(bvadd Start Start)
(bvmul Start Start)
(bvudiv Start Start)
(bvurem Start Start)
(bvlshr Start Start)
(bvashr Start Start)
(bvshl Start Start)
(bvsdiv Start Start)
(bvsrem Start Start)
(bvsub Start Start)
x
#x0000000000000000
#x0000000000000001
#x0000000000000002
#x0000000000000003
#x0000000000000004
#x0000000000000005
#x0000000000000006
#x0000000000000007
#x0000000000000008
#x0000000000000009
#x0000000000000009
#x0000000000000009
#x000000000000000A
#x000000000000000B
#x000000000000000C
#x000000000000000D
#x000000000000000E
#x000000000000000F
#x0000000000000010
(ite StartBool Start Start)
))
(StartBool Bool
((= Start Start)
(not StartBool)
(and StartBool StartBool)
(or StartBool StartBool)
))))
(constraint (= (f #x53ee2ed16eeeecc2) #x053ee2ed16eeeecc))
(constraint (= (f #xec1b547a5d5e5164) #x0ec1b547a5d5e516))
(constraint (= (f #x4722822ae0bb66ba) #x8e450455c176cd75))
(constraint (= (f #x395295bb82b630c9) #x0395295bb82b630c))
(constraint (= (f #xe149dd31788446d6) #x0e149dd31788446d))
(constraint (= (f #x63d4b7d058d069a7) #x063d4b7d058d069a))
(constraint (= (f #xb629929a63790e0a) #x6c532534c6f21c15))
(constraint (= (f #x0495b55e77760d18) #x00495b55e77760d1))
(constraint (= (f #xeea5b1bca2bc08e2) #x0eea5b1bca2bc08e))
(constraint (= (f #xe0e97096c3ece492) #x0e0e97096c3ece49))
(constraint (= (f #xb5dc2a1d0b967b96) #x0b5dc2a1d0b967b9))
(constraint (= (f #xd8e12e71a77ad3c0) #x0d8e12e71a77ad3b))
(constraint (= (f #x46e292676ee7ba6a) #x8dc524ceddcf74d5))
(constraint (= (f #x3301269c7ac9808b) #x66024d38f5930117))
(constraint (= (f #x84c4a72bb9bb92a8) #x09894e5773772551))
(constraint (= (f #x327b97b2020d0367) #x64f72f64041a06cf))
(constraint (= (f #x61e8ed250da4ba50) #x061e8ed250da4ba4))
(constraint (= (f #x264ee4e4262c8635) #x0264ee4e4262c863))
(constraint (= (f #x0466571ea1422222) #x00466571ea142222))
(constraint (= (f #xc1e99e1270e469b2) #x0c1e99e1270e469b))
(constraint (= (f #xe984b9e9a69d99eb) #xd30973d34d3b33d7))
(constraint (= (f #x1c7cae0bc98b025c) #x38f95c17931604b9))
(constraint (= (f #x268ea380e98d0e60) #x4d1d4701d31a1cc1))
(constraint (= (f #x22e9425be22bae26) #x45d284b7c4575c4d))
(constraint (= (f #xb5cec606b78a69cd) #x0b5cec606b78a69c))
(constraint (= (f #x4e8d1eeba2e57712) #x9d1a3dd745caee25))
(constraint (= (f #x31344ac9d965b5ed) #x62689593b2cb6bdb))
(constraint (= (f #xc9c70ebab63b2552) #x938e1d756c764aa5))
(constraint (= (f #x74e8cbb27e9d879c) #xe9d19764fd3b0f39))
(constraint (= (f #xa9430a5704035b42) #x528614ae0806b685))
(constraint (= (f #xd747ae0d0b925d93) #x0d747ae0d0b925d9))
(constraint (= (f #xe5e12749e2daeed8) #x0e5e12749e2daeed))
(constraint (= (f #xaae750c2ee5339e2) #x55cea185dca673c5))
(constraint (= (f #x4e0d4c7d83847ad0) #x04e0d4c7d83847ac))
(constraint (= (f #x84b6b3c741a7be0e) #x096d678e834f7c1d))
(constraint (= (f #x1e1046d1cab2e79a) #x01e1046d1cab2e79))
(constraint (= (f #x52eb7b8ac64e8006) #x052eb7b8ac64e800))
(constraint (= (f #x61e68ecc303346a7) #xc3cd1d9860668d4f))
(constraint (= (f #xee78b75c55e26abd) #x0ee78b75c55e26ab))
(constraint (= (f #x21727c0b6e96251d) #x021727c0b6e96251))
(constraint (= (f #xee72ae7ecbe81883) #x0ee72ae7ecbe8188))
(constraint (= (f #xe02ba8ec0bece751) #x0e02ba8ec0bece75))
(constraint (= (f #x2decbe436d32bb16) #x02decbe436d32bb1))
(constraint (= (f #x75381e46d7dae21c) #x075381e46d7dae21))
(constraint (= (f #xe97196c7376e48c5) #x0e97196c7376e48c))
(constraint (= (f #x0340dd07e3b5e0a0) #x0681ba0fc76bc141))
(constraint (= (f #x54118b737e243d9d) #x054118b737e243d9))
(constraint (= (f #xa3bae5cd6b34acaa) #x0a3bae5cd6b34aca))
(constraint (= (f #x7cb0b8c9b48a42b7) #x07cb0b8c9b48a42b))
(constraint (= (f #xbe882d1e26ed1ada) #x7d105a3c4dda35b5))
(constraint (= (f #xe5909c20baedd390) #xcb21384175dba721))
(constraint (= (f #xaa1174e57ea0abc2) #x0aa1174e57ea0abc))
(constraint (= (f #x07a9a10840cbb184) #x0f53421081976309))
(constraint (= (f #x523e152b9e07eecb) #xa47c2a573c0fdd97))
(constraint (= (f #x045c7628c87826c3) #x0045c7628c87826c))
(constraint (= (f #xae76367894d813dc) #x0ae76367894d813d))
(constraint (= (f #xd73ebd3366652dea) #xae7d7a66ccca5bd5))
(constraint (= (f #x802c015d88bc93cb) #x0802c015d88bc93c))
(constraint (= (f #x6e977d55e407eece) #xdd2efaabc80fdd9d))
(constraint (= (f #x76e50ae820e37b05) #xedca15d041c6f60b))
(constraint (= (f #x22c2a11542a042ea) #x022c2a11542a042e))
(constraint (= (f #xb9075d67d11737ae) #x720ebacfa22e6f5d))
(constraint (= (f #x92b4cec4ceecd9cd) #x092b4cec4ceecd9c))
(constraint (= (f #x8b094855b40beead) #x161290ab6817dd5b))
(constraint (= (f #xa4eeed0d65768ced) #x0a4eeed0d65768ce))
(constraint (= (f #x57cbec352283185b) #xaf97d86a450630b7))
(constraint (= (f #xb5827ca952bbbe58) #x6b04f952a5777cb1))
(constraint (= (f #x3832aeeb03b23c43) #x03832aeeb03b23c4))
(constraint (= (f #x21e84767a6b4c3eb) #x021e84767a6b4c3e))
(constraint (= (f #x82381ac97e534269) #x04703592fca684d3))
(constraint (= (f #x178890514aec8b34) #x0178890514aec8b3))
(constraint (= (f #x371c967047acb399) #x0371c967047acb39))
(constraint (= (f #x45c9514380554846) #x8b92a28700aa908d))
(constraint (= (f #x32d9e2e5e3bec060) #x032d9e2e5e3bec05))
(constraint (= (f #xeb348379531978b0) #xd66906f2a632f161))
(constraint (= (f #x7e9e37e0e2948d47) #x07e9e37e0e2948d4))
(constraint (= (f #x8c8dcb560512e928) #x08c8dcb560512e92))
(constraint (= (f #x516addc2d678352e) #x0516addc2d678352))
(constraint (= (f #x65014e719d617324) #xca029ce33ac2e649))
(constraint (= (f #x06b836e70dc95c90) #x0d706dce1b92b921))
(constraint (= (f #x33b96d68254e4e17) #x033b96d68254e4e1))
(constraint (= (f #x9ee648be0a81ace0) #x3dcc917c150359c1))
(constraint (= (f #xb94436e26ce5b7a2) #x72886dc4d9cb6f45))
(constraint (= (f #x4026390e69c011c6) #x04026390e69c011c))
(constraint (= (f #x3ae27d0511aee8a3) #x03ae27d0511aee8a))
(constraint (= (f #xd162ecb019600284) #x0d162ecb01960028))
(constraint (= (f #x0264a7e9349004ea) #x00264a7e9349004e))
(constraint (= (f #xa6e42d74ee921370) #x0a6e42d74ee92136))
(constraint (= (f #x3c893eee42cb1864) #x79127ddc859630c9))
(constraint (= (f #x8e26721917c86093) #x08e26721917c8609))
(constraint (= (f #x5e1eb7cebb07ee11) #xbc3d6f9d760fdc23))
(constraint (= (f #x05797aa3459dee1a) #x0af2f5468b3bdc35))
(constraint (= (f #x680b56d8eae0ee77) #x0680b56d8eae0ee7))
(constraint (= (f #x9e470294e626052e) #x09e470294e626052))
(constraint (= (f #x803a4180a5d4eb7e) #x0803a4180a5d4eb7))
(constraint (= (f #x60ac192c37bc981e) #x060ac192c37bc981))
(constraint (= (f #x53ca63b91d31664a) #xa794c7723a62cc95))
(constraint (= (f #x9808789e043ed16a) #x09808789e043ed16))
(constraint (= (f #x9c799e1eeb170891) #x38f33c3dd62e1123))
(constraint (= (f #x93d6bd9d37e2a09a) #x093d6bd9d37e2a09))
(check-synth)
(define-fun f_1 ((x (BitVec 64))) (BitVec 64) (ite (= (bvand #x000000000000000f x) #x0000000000000000) (ite (= (bvurem x #x0000000000000003) #x0000000000000001) (bvsub x (bvnot x)) (ite (= (bvurem x #x000000000000000b) #x0000000000000000) (bvsub x (bvnot x)) (bvnot (bvneg (bvudiv x #x0000000000000010))))) (ite (= (bvsrem x #x000000000000000f) #x0000000000000000) (bvudiv x #x0000000000000010) (ite (= (bvurem x #x000000000000000b) #x0000000000000001) (ite (= (bvsrem x #x0000000000000003) #x0000000000000000) (bvsub x (bvnot x)) (ite (= (bvor #x0000000000000001 x) x) (bvudiv x #x0000000000000010) (ite (= (bvurem x #x0000000000000003) #x0000000000000000) (ite (= (bvor #x0000000000000008 x) x) (ite (= (bvurem x #x0000000000000009) #x0000000000000000) (bvsub x (bvnot x)) (bvudiv x #x0000000000000010)) (bvsub x (bvnot x))) (bvsub x (bvnot x))))) (ite (= (bvsrem x #x0000000000000003) #x0000000000000000) (ite (= (bvor #x0000000000000002 x) x) (bvudiv x #x0000000000000010) (ite (= (bvurem x #x0000000000000009) #x0000000000000000) (bvsub x (bvnot x)) (ite (= (bvand #x0000000000000005 x) #x0000000000000001) (bvsub x (bvnot x)) (bvudiv x #x0000000000000010)))) (ite (= (bvor #x000000000000000a x) x) (ite (= (bvurem x #x0000000000000009) #x0000000000000000) (ite (= (bvor #x0000000000000006 x) x) (bvsub x (bvnot x)) (bvudiv x #x0000000000000010)) (ite (= (bvsrem x #x000000000000000d) #x0000000000000000) (bvudiv x #x0000000000000010) (ite (= (bvsrem x #x0000000000000005) #x0000000000000000) (ite (= (bvand #x0000000000000010 x) #x0000000000000000) (bvsub x (bvnot x)) (bvudiv x #x0000000000000010)) (bvsub x (bvnot x))))) (ite (= (bvand #x0000000000000005 x) #x0000000000000001) (ite (= (bvurem x #x0000000000000007) #x0000000000000001) (bvsub x (bvnot x)) (bvudiv x #x0000000000000010)) (ite (= (bvurem x #x000000000000000d) #x0000000000000000) (bvsub x (bvnot x)) (ite (= (bvurem x #x0000000000000003) #x0000000000000000) (ite (= (bvurem x #x000000000000000e) #x0000000000000000) (bvsub x (bvnot x)) (bvudiv x #x0000000000000010)) (ite (= (bvsrem x #x000000000000000d) #x0000000000000000) (bvudiv x #x0000000000000010) (ite (= (bvurem x #x0000000000000007) #x0000000000000001) (bvudiv x #x0000000000000010) (ite (= (bvurem x #x000000000000000a) #x0000000000000000) (bvsub x (bvnot x)) (ite (= (bvurem x #x000000000000000e) #x0000000000000000) (bvudiv x #x0000000000000010) (ite (= (bvsrem x #x0000000000000007) #x0000000000000000) (bvsub x (bvnot x)) (ite (= (bvand #x0000000000000010 x) #x0000000000000000) (ite (= (bvor #x0000000000000001 x) x) (bvsub x (bvnot x)) (ite (= (bvurem x #x0000000000000003) #x0000000000000001) (bvudiv x #x0000000000000010) (ite (= (bvand #x000000000000000a x) #x0000000000000000) (ite (= (bvashr x x) #x0000000000000000) (bvsub x (bvnot x)) (bvudiv x #x0000000000000010)) (bvsub x (bvnot x))))) (ite (= (bvand #x0000000000000005 x) #x0000000000000000) (bvsub x (bvnot x)) (bvudiv x #x0000000000000010)))))))))))))))))
